Журнал
Научно-технический вестник информационных технологий, механики и оптики
УДК:004.415.52, 004.434
Номер:4 (150)
Скачать PDF0 Кбайт
Верификация событийно-управляемых программных систем с использованием языка спецификации взаимодействующих автоматных объектов
Аннотация:
Введение. Язык спецификации Cooperative Interaction Automata Objects (CIAO) предназначен для описания поведения распределенных и параллельных систем, управляемых событиями. К этому классу систем относятся различные программно-аппаратные комплексы управления, контроля, сбора и обработки данных. Возможность автоматической проверки соответствия требованиям является желательным конкурентным преимуществом событийно-управляемых программных систем. Язык CIAO расширяет концепцию конечных автоматов (Unified Modeling Language, UML) возможностью кооперативного взаимодействия нескольких автоматов через строго определенные интерфейсы. Кооперативное взаимодействие автоматных объектов определяется схемой связи, которая связывает предоставленные и требуемые интерфейсы различных автоматных объектов. Таким образом, поведение системы в целом можно описать как набор протоколов выполнения, каждый из которых представляет собой последовательность вызовов интерфейса, возможно со сторожевыми условиями. Метод. Представлен набор протоколов с помощью семантического графа, в котором все возможные пути от начальных к конечным узлам определены последовательностью вызовов методов интерфейса. Благодаря тому, что интерфейсы заранее строго определены схемой связи, возможно автоматическое построение семантического графа по заданной системе взаимодействующих автоматных объектов. Для проверки поведения системы достаточно убедиться, что каждый путь в семантическом графе удовлетворяет требованиям. Системные требования формально описаны с помощью условных регулярных выражений, определяющих шаблоны допустимого и запрещенного поведения. Основные результаты. Предложены методы и алгоритмы, позволяющие автоматически проверить соответствие программ на языке CIAO заданным требованиям. Обсуждение. Разработанный метод сужает формализм для задания спецификаций до класса регулярных языков, а язык программирования — до языка с простой и предопределенной структурой. Во многих практических случаях этого достаточно для эффективной верификации.
Ключевые слова:
Постоянный URL
Статьи в номере
- Определение типа действия ингибиторов гидратообразования по их инфракрасным спектрам
- Спектроскопия комбинационного рассеяния света в исследованиях процессов инактивации бактериальных микроорганизмов
- Численное исследование влияния концентрации метгемоглобина в крови на поглощение света в коже человека
- Низкотемпературная ячейка для инфракрасных фурье-спектрометрических исследований углеводородных веществ
- Особенности выращивания твердых растворов Ga1–xInxAs на подложках GaAs в поле температурного градиента через тонкую газовую зону
- Усовершенствованный протокол безопасности на основе AES-GCM для защиты связи в интернете вещей
- Атаки на основе вредоносных возмущений на системы обработки изображений и методы защиты от них
- Сверхвысокое разрешение изображения магнитно-резонансной томографии головного мозга с использованием дискретного косинусного преобразования и сверточнойнейронной сети
- Метод аугментации текстовых данных с сохранением стиля речи и лексики персоны
- Интеллектуальная система адаптивного тестирования
- Нейросетевой метод визуального распознавания голосовых команд водителя с использованием механизма внимания
- Сегментация опухоли головного мозга на магнитно-резонансной томографии с использованием нечеткого деформируемого слияния и алгоритма Dolphin-SCA
- Оптимизация систем отслеживания человека в виртуальной реальности на основе нейросетевого подхода
- Погрешности алгоритма демодуляции с генерируемой фазой несущей, вносимые фильтром низкой частоты
- Моделирование процесса корректировки формы роторов шаровых гироскопов
- Метод пространственного мультиплексирования в многоантенных системах связи
- Математическое моделирование теплообменного аппарата с учетом сильной зависимости вязкости нефти от температуры
- Подход к формированию обобщенных параметров технического состояния сложных технических систем c использованием нейросетевых структур
- Численное моделирование газодинамики при работе широкодиапазонного ракетного сопла с пористой вставкой
- Точное решение задачи отражения ударной волны от стенки, экранированной слоем газовзвеси
- Адаптивный наблюдатель переменных состояния нелинейной нестационарной системы с неизвестными постоянными параметрами и запаздыванием в канале измерений
- RuLegalNER: новый датасет для распознавания именованных юридических сущностей на русском языке